$\forall$$A$:Type, ${\it eq}$:EqDecider($A$), $L_{1}$, $L_{2}$:($A$ List), $x$:$A$.
\\[0ex]($x$ $\in$ l\_intersection(${\it eq}$;$L_{1}$;$L_{2}$)) $\Leftarrow\!\Rightarrow$ (($x$ $\in$ $L_{1}$) \& ($x$ $\in$ $L_{2}$))